(* $Id: PFOLtoFOL.ml 74 2007-10-16 12:20:18Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open PFOLSyntax

let mk_type_constant s = 
  Var.Atom.freshb (PIdentifier.mk_value_id (Position.dummy, s))

let oterm_type_var = mk_type_constant "term"
let oterm_type = TVar oterm_type_var
let tarrow = mk_type_constant "tarrow"
let tcarrow = mk_type_constant "tcarrow"
let tparrow = mk_type_constant "tparrow"
let tpredicate = mk_type_constant "tpredicate"
let int_type = mk_type_constant "int"
let bool_type = mk_type_constant "bool"
let unit_type = mk_type_constant "unit"
let prop_type_var = mk_type_constant "prop"
let prop_type = Var prop_type_var

let mk_tapp t tys = App (t, tys)
let mk_tarrow ty1 ty2 = App (tarrow, [ ty1; ty2 ])
let mk_tcarrow ty1 ty2 = App (tcarrow, [ ty1; ty2 ])
let mk_tparrow ty1 ty2 = App (tparrow, [ ty1; ty2 ])
let mk_tpredicate ty1 ty2 = App (tpredicate, [ ty1; ty2 ])
let mk_prod_type tys = Prod (tys)

let mk_constant s = 
  Var.Atom.freshb (PIdentifier.mk_value_id (Position.dummy, s))

let sort = mk_constant "sort"
let bind_pred = mk_constant "bind"

let cons_decl (dec, q) = 
  ConsDecl (create_cons_decl_abs (dec, q))
    
let context c = 
  let values_decls = 
    List.fold_left (fun ds (v, i) ->
		      let ty = 
			TProd (Misc.repeat i (fun _ -> oterm_type))
		      in
			cons_decl 
			  (DVal (v, (create_type_scheme_abs ([], ty))),
			   ds))
      c
      [
	(tarrow, 2);
	(tcarrow, 2);
	(tparrow, 2);
	(tpredicate, 2);
	(int_type, 0);
	(bool_type, 0);
	(unit_type, 0);
	(sort, 2)
      ]
  in
  let bind_predicate_decl = 
    DPred (bind_pred, PredDec (create_predicate_type_scheme_abs ([], [ oterm_type ])))
  in
    cons_decl (DType (oterm_type_var, 0),
	       cons_decl (DType (prop_type_var, 0), 
			  cons_decl (bind_predicate_decl,  values_decls)))


let primitive_types = [ int_type; unit_type; bool_type ]

let mk_constant s = 
  Var.Atom.freshb (PIdentifier.mk_value_id (Position.dummy, s))

let sorted ty t = App (sort, [ ty; t ])

let is_primitive_type = function
  | Var x ->
      List.exists (fun y -> Var.Atom.equal x y) primitive_types
  | _ -> false

type env =
    {
      values     : (Var.Atom.t * term) list;
      types	 : (Var.Atom.t * term_type) list
    }

let empty = { values = []; types = [] }

let rec bind x ty env =
  { env with values = (x, term_type env ty) :: env.values }

and lookup x env = 
  List.assoc x env.values

and bind_type x arity env = 
  let kind = TProd (Misc.repeat arity (fun _ -> oterm_type)) in
    ({ env with types = (x, kind) :: env.types }, kind)

and lookup_type x env = 
  List.assoc x env.types

and predicate env = function
    | ForallTys abs ->
	let (ts, f) = open_polyf_abs abs in
	let (env, bs) = type_parameters env ts in
	let f = predicate env f in
	  Forall (create_forall_abs (bs, [], f))

    | Forall abs ->
	let (bs, ts, f) = open_forall_abs abs in
	let (env, bs) = bindings env bs in
	  Forall (create_forall_abs (bs, ts, predicate env f))

    | Exists abs ->
	let (bs, f) = open_exists_abs abs in
	let (env, bs) = bindings env bs in
	  Exists (create_exists_abs (bs, predicate env f))

    | LogicBinOpApp (op, lhs, rhs) ->
	LogicBinOpApp (op, predicate env lhs, predicate env rhs)

    | BinOpApp (op, lhs, rhs) ->
	BinOpApp (op, term env lhs, term env rhs)

    | Neg p ->
	Neg (predicate env p)

    | PApp (f, args) -> 
	PApp (f, List.map (term env) args)

    | PEq (lhs, rhs) -> 
	PEq (term env lhs, term env rhs)

    | PTrue ->
	PTrue

    | PFalse ->
	PFalse

    | Pre (f, t1, t2) ->
	Pre (f, term env t1, term env t2)

    | Post (f, t1, t2, t3) ->
	Post (f, term env t1, term env t2, term env t3)

    | Reify t ->
	Reify (term env t)

and binop = fun x -> x

and bindings env bs = 
  Misc.list_fold_map binding env bs

and binding env (x, ty) = 
  let env = bind x ty env in
    (env, (x, oterm_type))

and term env = function
  | Var x ->
      Var x

  | App (f, args) ->
      App (f, List.map (term env) args)

  | Prod ts ->
      let ts = List.map (term env) ts in
	Prod ts

  | Prim p ->
      Prim p

  | PrimApp (p, args) ->
      PrimApp (primitive p, List.map (term env) args)

  | PredObjectApp (obj, args) ->
      PredObjectApp (term env obj, List.map (term env) args)

  | Annot (t, ty) ->
      let oty = term_type env ty in
	sorted oty (term env t)

and primitive p = 
  match p with
  | PInt x -> p
  | PFalseBool
  | PTrueBool
  | PAdd
  | PSub
  | PMult
  | PDiv
  | PLessThanObj
  | PGreaterThanObj
  | PLessEqualThanObj
  | PGreaterEqualThanObj
  | PEqObj -> p

and type_of_primitive = function
  | PInt _ -> TPrimitive TInt
  | PFalseBool | PTrueBool -> TPrimitive TBool
  | _ -> assert false

and term_type env = function
  | TVar x -> 
      Var x 

  | TApp (tycon, ts) -> 
      mk_tapp tycon (List.map (term_type env) ts)

  | TArrow (t1, t2) -> 
      mk_tarrow (term_type env t1) (term_type env t2)

  | TCArrow (t1, t2) -> 
      mk_tcarrow (term_type env t1) (term_type env t2)

  | TPArrow (t1, t2) -> 
      mk_tparrow (term_type env t1) (term_type env t2)

  | TProd ts -> 
      mk_prod_type (List.map (term_type env) ts)

  | TPrimitive pt -> 
      primitive_type pt

  | TProp -> 
      prop_type

  | TPredicate (ty1, ty2) -> 
      mk_tpredicate (term_type env ty1) (term_type env ty2)

and primitive_type = function
  | TInt  -> Var (int_type)
  | TBool -> Var (bool_type)
  | TUnit -> Var (unit_type)

and declaration env = function
  | DType (ty, arity) -> 
      let (env, kind) = bind_type ty arity env in
	(env, [ DVal (ty, (create_type_scheme_abs ([], kind))) ])

  | DVal (v, s) -> 
      let (ts, ty) = open_type_scheme_abs s in
      let (env, tbs) = type_parameters env ts in
      let oty = term_type env ty in
      let env = bind v ty env in
	(env, 
	 [ DVal (v, (create_type_scheme_abs ([], oterm_type)));
(*	   DAxiom 
	     ([], 
	      Forall 
		(create_forall_abs (tbs, [],
				    PApp (bind_pred, [sorted oty (Var v)])))) *)
	 ])
		  
  | DPred (p, pdef) -> 
      (env, predicate_declaration env p pdef)

  | DAxiom (ts, pdef) -> 
      let (env, bs) = type_parameters env ts in
      let pdef = predicate env pdef in
	(env, [ DAxiom ([], Forall (create_forall_abs (bs, [], pdef))) ])

and predicate_declaration env p = function
  | PredDef abs ->
      let (ts, bs, def) = open_predicate_def_abs abs in
      let xs = List.map (fun (x, ty) -> sorted (term_type env ty) (Var x)) bs in
      let s = 
	create_predicate_type_scheme_abs ([], 
					  List.map (fun _ -> oterm_type) bs) 
      in
      let (env, bts) = type_parameters env ts in
      let (env, bs) = bindings env bs in
      let def_pred = 
	Forall (create_forall_abs 
		  (bts @ bs, [], 
		   LogicBinOpApp (Equiv, PApp (p, xs), predicate env def)))
      in
	[ DPred (p, PredDec s); DAxiom ([], def_pred) ]

  | PredDec s -> 
      [ DPred (p, PredDec (predicate_type_scheme env s)) ]

and type_scheme abs =
(*  let (ts, _) = open_type_scheme_abs abs in *)
    create_type_scheme_abs ([], oterm_type)

and predicate_type_scheme env s = 
  let (ts, tys) = open_predicate_type_scheme_abs s in
    create_predicate_type_scheme_abs ([], List.map (fun _ -> oterm_type) tys)

and type_parameters env ts = 
  Misc.list_fold_map type_parameter env ts

and type_parameter env t = 
  let (env, oty) = bind_type t 0 env in
    (env, (t, oty))

and query env = function
  | Goal p ->
      Goal (predicate env p)

  | ConsDecl abs ->
      let (dec, q) = open_cons_decl_abs abs in
      let (env, decs) = declaration env dec in 
	List.fold_left (fun q dec ->ConsDecl (create_cons_decl_abs (dec, q)))
	  (query env q) (List.rev decs)

let query q = context (query empty q)
